(set-option :model_validate true)
(set-option :rewriter.cache_all true)
(set-option :smt.arith.solver 4)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i6 Int)
(declare-const i8 Int)
(declare-const i9 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const i16 Int)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(push 1)
(declare-const i17 Int)
(push 1)
(declare-const v12 Bool)
(declare-const i18 Int)
(declare-const v13 Bool)
(assert (exists ((q0 Int) (q1 Bool) (q2 Bool) (q3 Bool)) (=> (<= q0 q0) (or q2 v8 v9 q3 q1 v12 q3))))
(declare-const v14 Bool)
(assert (or v1 v4 (=> v11 v0)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (=> v1 v4) (<= i4 i13)))
(assert (or (>= 12 i2) v1 (<= i4 i13)))
(assert (or v2 (<= i4 i13) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v13 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v2))
(assert (or v4 (<= i4 i13) v4))
(assert (or v1 (<= i4 i13) (=> v1 v4)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (<= i4 i13) (=> v11 v0)))
(assert (or (=> v1 v4) v13 v2))
(assert (or v5 (<= i4 i13) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (=> v1 v4) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (=> v1 v4) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v1))
(assert (or (>= 12 i2) v13 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (>= 12 i2) (=> v1 v4) (>= 12 i2)))
(assert (or v13 (>= 12 i2) v5))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v13 v1))
(assert (or v2 v5 (=> v1 v4)))
(assert (or (=> v11 v0) (=> v11 v0) v5))
(assert (or (<= i4 i13) (=> v1 v4) v13))
(assert (or v5 v4 v1))
(assert (or v2 v2 v5))
(assert (or v5 (<= i4 i13) v13))
(assert (or v5 v4 v4))
(assert (or v4 v2 (>= 12 i2)))
(assert (or v1 v4 (<= i4 i13)))
(assert (or v4 v2 v5))
(assert (or v2 v1 (=> v11 v0)))
(assert (or (<= i4 i13) v5 (=> v1 v4)))
(assert (or v1 (=> v11 v0) v1))
(assert (or (>= 12 i2) v2 v13))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (>= 12 i2) (=> v1 v4)))
(assert (or v2 v1 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v1 (=> v11 v0) v13))
(assert (or v5 v1 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v4 v2 (=> v11 v0)))
(assert (or v5 v2 (=> v1 v4)))
(assert (or v4 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v4 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v1 v2))
(assert (or (<= i4 i13) v2 (<= i4 i13)))
(assert (or (=> v1 v4) (=> v11 v0) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (=> v11 v0) v5 v1))
(assert (or v13 (>= 12 i2) v2))
(assert (or (>= 12 i2) (=> v11 v0) (=> v11 v0)))
(assert (or (>= 12 i2) (<= i4 i13) v4))
(assert (or v4 v2 v2))
(assert (or (=> v1 v4) v1 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v1 v4 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v1 (=> v11 v0)))
(assert (or (>= 12 i2) v1 (<= i4 i13)))
(assert (or v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or (=> v1 v4) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v1))
(assert (or v4 (>= 12 i2) (=> v11 v0)))
(assert (or v13 (<= i4 i13) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (<= i4 i13) (=> v11 v0) v13))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v4 (=> v11 v0)))
(assert (or v1 v13 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v13 (<= i4 i13) v4))
(assert (or (>= 12 i2) v2 v4))
(assert (or (=> v1 v4) (<= i4 i13) v2))
(assert (or v13 v4 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v13 v2 v13))
(assert (or (>= 12 i2) v5 v1))
(assert (or v4 (=> v1 v4) (=> v1 v4)))
(assert (or (>= 12 i2) (>= 12 i2) v1))
(assert (or v4 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (<= i4 i13) (>= 12 i2)))
(assert (or v5 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (=> v11 v0)))
(assert (or v5 (=> v1 v4) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v13 (=> v11 v0) v5))
(assert (or (>= 12 i2) v1 v13))
(assert (or (=> v11 v0) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or v1 (=> v1 v4) v13))
(assert (or (<= i4 i13) (<= i4 i13) (=> v11 v0)))
(assert (or v5 (=> v1 v4) v5))
(assert (or (<= i4 i13) v2 (>= 12 i2)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v2 v2))
(assert (or v4 (=> v11 v0) v5))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (>= 12 i2) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v13 v2 v4))
(assert (or (>= 12 i2) (=> v1 v4) (>= 12 i2)))
(assert (or v4 v5 (=> v11 v0)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4) v13))
(assert (or v4 (<= i4 i13) v5))
(assert (or v5 (>= 12 i2) (=> v11 v0)))
(assert (or v2 v1 v5))
(assert (or (<= i4 i13) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (>= 12 i2) v4 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v2 v5 v2))
(assert (or v5 (=> v11 v0) v13))
(assert (or (>= 12 i2) (=> v1 v4) v1))
(assert (or v2 (=> v1 v4) (=> v1 v4)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v1 v5))
(assert (or (<= i4 i13) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v4 v13))
(assert (or v5 (=> v1 v4) v5))
(assert (or (>= 12 i2) v4 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v13 v13 v1))
(assert (or v4 v13 v5))
(assert (or (>= 12 i2) v13 v1))
(assert (or v5 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (<= i4 i13)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v2 (>= 12 i2)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v11 v0) (>= 12 i2)))
(assert (or v2 (<= i4 i13) v5))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4) v13))
(assert (or (>= 12 i2) (=> v1 v4) v1))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (>= 12 i2) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (=> v11 v0) (=> v11 v0) (=> v1 v4)))
(assert (or (<= i4 i13) v1 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v2 v4))
(assert (or v5 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v1))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (=> v11 v0) v2))
(assert (or v1 (=> v11 v0) v1))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v11 v0) v13))
(assert (or (=> v1 v4) (>= 12 i2) (>= 12 i2)))
(assert (or (>= 12 i2) v2 v2))
(assert (or v1 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (<= i4 i13)))
(assert (or v5 (=> v1 v4) v4))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (<= i4 i13) (=> v1 v4)))
(assert (or (=> v1 v4) (=> v1 v4) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v13 v13 (=> v1 v4)))
(assert (or (>= 12 i2) v13 (=> v1 v4)))
(assert (or v1 v4 v2))
(assert (or (<= i4 i13) (=> v11 v0) (=> v1 v4)))
(assert (or v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (<= i4 i13)))
(assert (or (=> v1 v4) v13 v2))
(assert (or v1 v2 (=> v1 v4)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (>= 12 i2) (>= 12 i2)))
(assert (or (=> v1 v4) (>= 12 i2) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v4 (=> v11 v0) v13))
(assert (or (=> v1 v4) (=> v11 v0) (=> v1 v4)))
(assert (or v13 v13 (<= i4 i13)))
(assert (or (=> v1 v4) (>= 12 i2) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v2 v1 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v5 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (=> v1 v4) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v11 v0)))
(assert (or v4 (=> v11 v0) (=> v1 v4)))
(assert (or (=> v1 v4) (<= i4 i13) (=> v1 v4)))
(assert (or (>= 12 i2) (=> v11 v0) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v5 v5 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v5 v2))
(assert (or (=> v11 v0) (=> v1 v4) (>= 12 i2)))
(assert (or v4 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v1 v2 v4))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v4 (>= 12 i2)))
(assert (or v4 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (>= 12 i2)))
(assert (or v1 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v13))
(assert (or (<= i4 i13) (=> v11 v0) (<= i4 i13)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v1))
(assert (or v1 v13 (>= 12 i2)))
(assert (or (=> v1 v4) (>= 12 i2) v13))
(assert (or (<= i4 i13) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or (=> v11 v0) (>= 12 i2) v1))
(assert (or v5 (>= 12 i2) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v4 v5 (<= i4 i13)))
(assert (or (>= 12 i2) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or v5 (>= 12 i2) (=> v11 v0)))
(assert (or (=> v1 v4) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (>= 12 i2)))
(assert (or v5 v1 v1))
(assert (or v5 v13 v4))
(assert (or v5 (<= i4 i13) (=> v1 v4)))
(assert (or v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v4))
(assert (or v1 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v5))
(assert (or v13 (>= 12 i2) (=> v1 v4)))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v2 v1))
(assert (or v13 v1 v1))
(assert (or (<= i4 i13) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v13 (=> v1 v4) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (<= i4 i13) v4 (>= 12 i2)))
(assert (or v5 v2 v4))
(assert (or (=> v11 v0) (=> v11 v0) (>= 12 i2)))
(assert (or (>= 12 i2) (>= 12 i2) (=> v11 v0)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v1 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v4 v1))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v2 (<= i4 i13)))
(assert (or (>= 12 i2) v4 (>= 12 i2)))
(assert (or (<= i4 i13) (=> v1 v4) v4))
(assert (or v1 v2 v13))
(assert (or v13 (=> v1 v4) (<= i4 i13)))
(assert (or (<= i4 i13) (>= 12 i2) v13))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v5 (=> v11 v0)))
(assert (or v13 (<= i4 i13) v13))
(assert (or (=> v11 v0) v5 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (>= 12 i2) (=> v1 v4) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (<= i4 i13) v13 v13))
(assert (or v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or v1 v2 v13))
(assert (or v2 v2 v1))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (=> v11 v0)))
(assert (or v1 v2 (>= 12 i2)))
(assert (or (=> v1 v4) (>= 12 i2) v1))
(assert (or v2 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (<= i4 i13)))
(assert (or v4 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (=> v11 v0)))
(assert (or (<= i4 i13) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v2))
(assert (or v4 v4 v4))
(assert (or v13 (=> v1 v4) v13))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or (=> v11 v0) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v5))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (=> v1 v4)))
(assert (or v2 (=> v1 v4) (=> v11 v0)))
(assert (or (>= 12 i2) (=> v11 v0) v1))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v4 (>= 12 i2)))
(assert (or (=> v11 v0) (=> v11 v0) v4))
(assert (or (>= 12 i2) (<= i4 i13) (=> v11 v0)))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (<= i4 i13) v4))
(assert (or v13 (<= i4 i13) v1))
(assert (or v2 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v2))
(assert (or v2 v5 v1))
(assert (or v5 (=> v1 v4) v1))
(assert (or v4 (<= i4 i13) (=> v1 v4)))
(assert (or v2 (=> v11 v0) v13))
(assert (or v4 (>= 12 i2) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v13 (<= i4 i13) (=> v11 v0)))
(assert (or (=> v11 v0) (=> v11 v0) (=> v11 v0)))
(assert (or v13 (>= 12 i2) v13))
(assert (or (<= i4 i13) v2 v2))
(assert (or v5 (<= i4 i13) v13))
(assert (or (=> v1 v4) v1 v5))
(assert (or v5 (>= 12 i2) v4))
(assert (or (>= 12 i2) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) v1))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v1 v4))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v1 v2))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v1 v13))
(assert (or (=> v1 v4) (=> v11 v0) v5))
(assert (or v2 (=> v11 v0) v5))
(assert (or v1 v4 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or (=> v1 v4) (<= i4 i13) v2))
(assert (or v13 v1 (=> v1 v4)))
(assert (or v13 (<= i4 i13) v13))
(assert (or (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (=> v11 v0) v1))
(assert (or (=> v11 v0) (=> v11 v0) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v2 v4 (=> v1 v4)))
(assert (or v13 (=> v11 v0) v1))
(assert (or v2 v1 v4))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (>= 12 i2)))
(assert (or v13 v4 (<= i4 i13)))
(assert (or v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v2))
(assert (or v1 v1 v4))
(assert (or v4 v5 (<= i4 i13)))
(assert (or (=> v11 v0) v4 (>= 12 i2)))
(assert (or v5 (=> v11 v0) v5))
(assert (or (=> v1 v4) v1 v5))
(assert (or v4 (<= i4 i13) (>= 12 i2)))
(assert (or v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4)))
(assert (or v13 (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8) (and (distinct i11 i13) v2 (=> v2 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))) v2 v2 v8)))
(assert (or v13 (<= i4 i13) v5))
(assert (or v5 (=> v1 v4) v4))
(assert (or (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) (=> v1 v4) v13))
(assert (or (>= 12 i2) v5 (>= 12 i2)))
(assert (or v1 (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v2))
(assert (or (>= 12 i2) v1 (=> v1 v4)))
(assert (or v5 (=> v1 v4) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or v1 (=> v11 v0) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13))))
(assert (or (=> v1 v4) (and v5 v10 (distinct i11 i13) (>= 12 i2) v0 v1 v2 (=> v1 v4) (= i8 i13)) v4))
(assert (or (>= 12 i2) v5 (=> v11 v0)))
(assert (or (=> v1 v4) (=> v11 v0) v4))
(assert (or (>= 12 i2) v5 v13))
(assert (or v4 (<= i4 i13) (>= 12 i2)))
(assert (or (=> v1 v4) v1 v1))
(assert (or (>= 12 i2) v4 v13))
(assert (or (=> v11 v0) v2 (=> v11 v0)))
(assert (or (=> v11 v0) (=> v1 v4) v13))
(check-sat)
(exit)
